\begin{tabbing}
$\forall$$C$:es\_realizer\{i:l\}. 
\\[0ex]R{-}sub\=\{i:l\}\+
\\[0ex]($C$; $C$)
\-\\[0ex]$\wedge$ \=($\forall$$A$:es\_realizer\{i:l\}. \+
\\[0ex]R{-}sub\=\{i:l\}\+
\\[0ex]($C$; $A$)
\-\\[0ex]$\Rightarrow$ ($\forall$$B$:es\_realizer\{i:l\}. R{-}sub\{i:l\}($C$; Rplus($A$; $B$)) $\wedge$ R{-}sub\{i:l\}($C$; Rplus($B$; $A$))))
\-
\end{tabbing}